FDL - Step of Proof: adjacent-before

Step of Proof: adjacent-before

Inference at * 1 2
Iof proof for Lemma adjacent-before:

1. T : Type
2. L : T List
3. x : T
4. y : T
5. i : {0..(||L|| - 1)

}
6. x = L[i]
7. y = L[(i+1)]
8.

i@0:{0..1

}. if (i@0 =

0) then i else i+1 fi < if (i@0+1 =

0) then i else i+1 fi
9. j : {0..2

}

[x; y][j] = L[if (j =

0) then i else i+1 fi ]

by ((((CaseNat 0 `j')

CollapseTHEN (((Reduce 0)

CollapseTHEN ((Try (Trivial))

))

)

CoCollapseTHEN (((((CaseNat 1 `j')

CollapseTHEN (((Reduce 0)

CollapseTHEN ((Try (Trivial))

))

C))

)

CollapseTHEN (Auto'))

))